i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{k:Knd|
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{(k 
ks)}
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(
decl-state(ds)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(ma-valtype(da; k)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(TT).
(
(
fpf-dom(id-deq; x; ds)))
(A:es_realizer{i:l}.
R-Feasible{i:l}
R-Feasible(A)
((R-occurs(A; i; x)))
fpf-compatible(Id; x.Type; id-deq; ds; R-ds(A; i))
fpf-compatible(Knd; k.Type; Kind-deq; da; R-da(A; i))
l_all(ks;
l_all(Knd;
l_all(k.((isrcv(k))
l_all( subtype_rel(fpf-cap(R-da(A; source(lnk(k))); Kind-deq; k; void); ma-valtype(da; k))))
l_all(ks; Knd; k.(fpf-dom(Kind-deq; k; da)))
(k:Knd. (k ks) ((write-restricted(A; i; k))))
(y:Id.
(fpf-dom(id-deq; y; fpf-join(id-deq; ds; fpf-single(x; T))))
((read-restricted(A; i; y))))
R-compat{i:l}
R-compat(R-state-var(i; ds; da; x; T; ks; tr); A)) 
x. t(x)
Q
